\section {Metóda rezolvent pre logiku 1. rádu}

\begin{definicia}[Spojenie]
%%% {{{
    Nech $C$ je klauzula, ktorá obsahuje dva alebo viac literálov 
    (a tie pozostávajú z rovnakého predikátu len s inými parametrami).
    Ak tieto literály majú najvšeobecnejší unifikátor $\sigma$, 
    tak $C\sigma$ sa nazývame spojením $C$. 
    
    Ak $C\sigma$ je jednotková klauzula, tak $C\sigma$ nazývame tiež
    jednotkovým spojením $C$.
%%% }}}
\end{definicia}

\begin{priklad}
    Uvažujme klauzulu $C$, ktorá vyzerá nasledovne: 
    $C = \{ P(x) \lor P(f(y)) \lor \neg Q(x)\}$. Zoberme literály
    $P(x)$ a $P(f(y))$. Ich najvšeobecnejší unifikátor je
    $\sigma=\{ f(y) / x \}$. Potom spojenie je 
    $C\sigma = \{P(f(y)) \lor \neg Q(x) \}$.
\end{priklad}

\begin{definicia}[binárna rezolventa]
%%% {{{
    Nech $C_1$ a $C_2$ sú dve klauzuly (budeme ich nazývať predpoklady), 
    ktoré nemajú spoločné premenné. Nech $L_1 \in C_1$ a $L_2 \in C_2$ 
    sú dva literály. Ak $L_1$ a $\neg L_2$ majú 
    najvšeobecnejší unifikátor $\sigma$, tak výraz
    \begin{equation*}
        (C_1\sigma - L_1\sigma) \union (C_2\sigma - L_2\sigma)
    \end{equation*}
    sa nazýva binárnou rezolventou.\footnote{Za pozornosť stojí fakt, že
    vo všeobecnosti $(C\sigma - L\sigma) \ne (C-L)\sigma$.} 
    Literály $L_1$ a $L_2$ môžeme vynechať a nazývame ich nadbytočné.
%%% }}}
\end{definicia}

\begin{priklad}
    Majme $C_1 = P(x) \lor Q(x)$ a $C_2 = \neg P(a) \lor R(x)$, 
    čo budú predpoklady. Na to, aby sme mohli previesť operáciu
    binárnej rezolventy, musíme najskôr premenovať premenné v druhom
    výraze, aby boli rôzne od tých v prvom. Máme teda
    $C_2' = \neg P(a) \lor R(y)$.

    Uvažujme teraz klauzuly $L_1 = P(x)$ a $L_2 = \neg P(a)$.
    Ich najvšeobecnejší unifikátor je $\sigma = \{a/x\}$.

    Binárna rezolventa $C_1$ a $C_2$ je
    \begin{equation*}
    \begin{split}
        (C_1\sigma - L_1\sigma) \union (C_2\sigma - L_2\sigma) 
        &= (\{P(a),\ Q(a))\} - \{P(a)\}) \union
            (\{\neg P(a),\ R(y)\}-\{\neg P(a)\}) \\
        &= Q(a)\lor R(y)
    \end{split}
    \end{equation*}
    Nadbytočné literály sú $P(x), \neg P(a)$.
\end{priklad}

\begin{definicia}[Rezolventa logiky 1. rádu] 
%%% {{{
    Rezolventou z predpokladov $C_1$ a $C_2$ definujeme ako jednu z
    nasledujúcich binárnych rezolvent:
    \begin{enumerate}
        \item Binárna rezolventa $C_1$ a $C_2$
        \item Binárna rezolventa $C_1$ a spojenia $C_2$
        \item Binárna rezolventa spojenia $C_1$ a $C_2$
        \item Binárna rezolventa spojenia $C_1$ a spojenia $C_2$
    \end{enumerate}
%%% }}}
\end{definicia}

\begin{priklad}
    Uvažujme $C_1 = P(x) \lor P(f(y))\lor R(g(y))$,
             $C_2 = \neg P(f(g(a)) \lor Q(b)$.

    Spojenie $C_1$ je $C_1': P(f(y)) \lor R(g(y))$.
    Binárna rezolventa $C_1'$ a $C_2$ (a tým pádom rezolventa
    $C_1,C_2$) bude $R(g(g(a))) \lor Q(b)$.
\end{priklad}

Ešte predtým, než sa plne vrhneme do dokazovania úplnosti metódy
rezolvent, uvedieme si príklady na osvieženie pamäti.

\begin{priklad}
    \label{prikl:rezolv_pred}
    Majme množinu klauzúl 
    $S=\{P,\ \neg P\lor Q,\ \neg P \lor \neg Q\}$.
    Prislúchajúca herbrandovská báza je $\{P, Q\}$.
    Množine klauzúl $S$ zodpovedá úplný sémantický strom $T$
    naznačený na obrázku \ref{fig:rezolv_pred_prikl}. 
    
    K úplnému stromu $T$ môžeme zostrojiť uzavretý sémantický strom v ktorom
    každá vetva sa končí odmietajúcim vrcholom, teda odmieta niektorú
    z klauzúl z $S$.
    Vieme, že žiadna z tých interpretácií, ktoré končia v listoch, 
    nie je splniteľná. 

    Následne, strom $T'$ môžeme postupne pravidlom rezolventy
    upravovať -- klauzuly $\neg P \lor \neg Q$,
    $\neg P \lor Q$ obsahujú kontrárnu dvojicu $\neg Q,Q$.
    Ich rezolventa je $\neg P$. Množinu $S$ teda môžeme obohatiť a
    dostaneme $S''=S \union \{ \neg P \}$. Môžeme tiež upraviť aj
    strom $T'$ a dostávame $T''$.

    Pokračujme ďalej: $P, \neg P$ sú kontrárna dvojica a ich
    rezolventou je $\eps$. Dostávame strom $T'''$.

    Dospeli sme teda k tomu, že množina klauzúl $S$ je nesplniteľná.
    Zároveň si môžeme všimnúť, že každým aplikovaním pravidla
    rezolventy zmenšujeme strom.
    \begin{figure}
        \centering
        %%% {{{
        \subfigure[$T$]{
            \imageontop{
                \includegraphics{img/13/priklad.1.mps}
            }
        }
        \subfigure[$T'$]{
            \imageontop{
                \includegraphics{img/13/priklad.2.mps}
            }
        }
        \vskip 1.5cm
        \subfigure[$T''$]{
            \imageontop{
                \includegraphics{img/13/priklad.3.mps}
            }
        }
        \subfigure[$T'''$]{
            \hskip 2cm
            \imageontop{
                \includegraphics{img/13/priklad.4.mps}
            }
        }
        %%% }}}
        \caption{Stromy z príkladu \ref{prikl:rezolv_pred}}
        \label{fig:rezolv_pred_prikl}
    \end{figure}
\end{priklad}

\begin{priklad}[Opakovanie z úvodu k substitúcii]
%%% {{{
    Uvažujme dve klauzuly $C_1=P(x) \lor Q(x)$, 
    $C_2 = \neg P(f(x)) \lor R(x)$.

    V nich neexistuje žiadna kontrárna dvojica. Nahradením
    $x$ za $f(a)$ resp. $a$ 
    dostaneme základné inštancie
    $C_1'=P(f(a)) \lor Q(f(a))$, 
    $C_2'=\neg P(f(a)) \lor R(a)$.
    Teraz môžeme vypočítať rezolventu $Q(f(a)) \lor R(a)$.

    Mohli by sme postupovať aj všeobecnejšie -- nahraďme $x$ za $f(x)$ v
    prvej klauzule a dostávame
    $C_1^*= P(f(x)) \lor Q(f(x))$, $C_2^*= \neg P(f(x)) \lor R(x)$.

    Rezolventa potom bude $C^*= Q(f(x)) \lor R(x)$.
    Vidíme teda, že sme získali 2 rôzne rezolventy, jednu viac všeobecnú
    ako druhú.
%%% }}}
\end{priklad}

\subsubsection{Úplnosť metódy rezolvent}
Metódu rezolvent zaviedol roku 1965 Robinson.
Táto metóda je omnoho efektívnejšia ako pravidlá, ktoré zaviedli
Davis a Putnam. Veľmi dôležitým aspektom je hlavne to, že metóda
je úplná:
Ak množina klauzúl nie je splniteľná, potom metódou rezolvent z nej vždy
môžeme dostať prázdnu klauzulu 
(a teda formula nie je splniteľná v žiadnej interpretácii). 

\begin{lema}
    Nech $C_1'$ a $C_2'$ sú inštancie klauzúl $C_1$ resp. $C_2$.
    Ak $C'$ je rezolventa $C_1'$ a $C_2'$,
    tak potom existuje rezolventa\footnote{Na prednáške to bolo
        prezentované takto. Je však evidentné, že to malo byť
        formulované ``existuje rezolventa $C$ taká, že pre ľubovoľné
        inštancie $C_1',C_2'$ je $C'$ inštancia $C$''. Inak povedané,
        $C$ bude najvšeobecnejšia rezolventa a bude nezávislá od voľby
        základných inštancií $C_1',C_2'$.}
    $C$ klauzúl $C_1$ a $C_2$, 
    že $C'$ je inštancia $C$. 
\end{lema}

\begin{dokaz}
%%% {{{
    Ak je treba, ako prvý krok premenujeme premenné v $C_1$ a $C_2$
    aby boli rôzne (samozrejme, rovnaké premenovanie spravíme aj v
    inštanciách $C_1',C_2'$).
    Nech teraz $L_1'$ a $L_2'$ sú literály v $C_1',C_2'$, 
    ktoré môžeme vynechať (sú nadbytočné).
    Zoberme ich najvšeobecnejší unifikátor $\nu$ a binárna rezolventa
    $C'$ bude
    \begin{equation*}
        C' = (C_1' \nu - L_1'\nu) \union ( C_2'\nu - L_2'\nu)
    \end{equation*}

    $C_1'$, $C_2'$ sú inštancie $C_1$ a $C_2$ a teda existuje
    substitúcia\footnote{Poznamenávame, že $C_1$ a $C_2$ majú rôzne
    premenné a teda túto substitúciu získame ako zloženie
    individuálnych substitúcii pre jednotlivé klauzuly} 
    $\Theta$ taká, že platí:
    \begin{align*}
        C_1' &= C_1 \Theta \\
        C_2' &= C_2 \Theta
    \end{align*}

    Označme si teraz literály z $C_i$, ktoré
    zodpovedajú po substituovaní substitúciou $\Theta$ literálu $L_i'$ ako
    $L^1_i, L^2_i, \ldots, L^{r_i}_i$ kde $i=1,2$.
    Teda platí
    \begin{equation*}
        L^1_i \Theta = L^2_i \Theta = \cdots = L^{r_i}_i\Theta=L'_i
    \end{equation*}
    Ďalej si označme najvšeobecnejší unifikátor pre 
    $\{ L^1_i, L^2_i, \dots, L^{r_i}_i\}$ ako $\lambda_i$.
    Platí
    \begin{equation*}
        L^1_i \lambda_i = L^2_i \lambda_i = \cdots 
        =L^{r_i}_i\lambda_i=L_i
        .\footnote{Pozor, zmizla nám čiarka z $L_i$ oproti
        predchádzajúcej rovnici}
    \end{equation*}    
    Pretože $\lambda_i$ je najvšeobecnejší unifikátor, 
    pre vhodnú substitúciu $\xi$ platí:
    \begin{equation*}
        L_i' = L^j_i \Theta = L^j_i (\lambda_i \circ \xi) = 
        (L^j_i\lambda_i)\xi = L_i \xi
    \end{equation*}

    Pre pohodlnosť označme $\lambda = \lambda_1 \union \lambda_2$.
    Z predpokladov vety je jasné, že $L_1', \neg L_2'$ sú
    unifikovateľné. Označme ich najvšeobecnejší unifikátor 
    ako $\sigma$.
    Teraz pozor, zamerajme sa na spojenie $C_1 \lambda_1$ a $C_2
    \lambda_2$. Hlaďanú najvšeobecnejšiu rezolventu zostrojíme práve
    pomocou nich:
    \begin{equation*}
    \begin{split}
    C &= ((C_1\lambda)\sigma - L_1\sigma) \union 
            ((C_2\lambda_2)\sigma-L_2\sigma) \\
      &= ((C_1\lambda)\sigma - (\{L^1_1, L^2_1, \dots, L^{r_1}_1 \}
        \lambda )\sigma) \union
        ((C_2\lambda)\sigma - (\{L^1_2, L^2_2, \dots, L^{r_2}_2 \}
        \lambda )\sigma) \\
      &= (C_1 (\lambda \circ \sigma) -
            \{ L^1_1, \dots, L^{r_1}_1 \} (\lambda\circ\sigma)) \union
         (C_2  (\lambda\circ\sigma) - 
            \{L^1_2, \dots, L^{r_2}_1\}(\lambda\circ\sigma))
    \end{split}
    \end{equation*}

    Na záver ešte potrebujeme overiť, že $C'$ je inštancia $C$.
    \begin{equation*}
    \begin{split}
        C' &= (C_1' \nu - L_1' \nu) \cup (C_2'\nu - L_2'\nu) \\
          &= ((C_1\Theta)\nu - 
                (\{L^1_1, \dots ,L^{r_1}_1\}\Theta)\nu) \union
             ((C_2\Theta)\nu - 
                (\{L^1_2, L^2_2, \ldots, L^{r_2}_2\}\Theta )\nu) \\
          &= (C_1(\Theta\circ\nu) - 
                \{L^1_1, \dots, L^{r_1}_1\} (\Theta\circ\nu)) \union
             (C_2(\Theta\circ\nu) - 
                \{L^1_2, \dots, L^{r_2}_2\} (\Theta\circ\nu))
    \end{split}
    \end{equation*}

    Lenže vieme, že $\lambda \circ \sigma$ je všeobecnejšie
    ako $\theta \circ \nu$, pretože
    $\lambda$ je všeobecnejší unifikátor ako $\Theta$ a 
    $\sigma$ je všebecnejší unifikátor ako $\nu$.
    Tým pádom $C'$ je naozaj inštancia $C$.\footnote{Ešte by sme
        mohli mať zlé svedomie z toho, čo na to povie množinové mínus,
        na ktoré sme v minulosti upozorňovali. Čitateľ sa môže sám
        presvedčiť, že v tomto prípade je to naozaj v poriadku}
    \\
%%% }}}
\end{dokaz}

\begin{veta}[Úplnosť metódy rezolvent] 
    Množina klauzúl $S$ nie je splniteľná $\iff$ 
    existuje odvodenie prázdnej klauzuly $\eps$ z $S$.
\end{veta}

\begin{dokaz}
\noindent
    \begin{itemize}
    \item[$\Leftarrow:$]
        Budeme ukazovať sporom.
        Predpokladajme, že v $S$ existuje odvodenie prázdnej klauzuly $\eps$. 
        Teda existuje postupnosť rezolvent $R_1, R_2, \dots, R_n$ 
        (medzi nimi niekde bude aj $\eps$, zrejme môžeme predpokladať
        $R_n = \eps$).

        Kvôli sporu predpokladáme, že $S$ je splniteľná, 
        teda existuje jej model $\mathcal{M}$, ktorý
        vyhovuje všetkým klauzuliam z $S$. Ako sme predtým dokázali,
        pravidlo rezolventy je korektné pravidlo a teda, ak sú
        $C_1$, $C_2$ ľubovoľné klauzuly z $S$ a $C$ je ich rezolventa,
        zo splniteľnosti $C_1$, $C_2$ vyplýva aj splniteľnosť $C$.
        Ak teda prejdeme celé rezolvenčné odvodenie $R_1,R_2,\dots,R_n$,
        postupne ukážeme, že $R_n=\eps$ je splniteľná klauzula. Spor.

    \item[$\Rightarrow:$] Ak
        predpokladáme, že $S$ nie je splniteľná,
        potom podľa Herbrandovej vety (1. variant),
        nie je splniteľná práve vtedy, keď je možné jej priradiť konečný
        uzavretý sémantický strom $T$. Bez ujmy na všeobecnosti budeme
        ďalej predpokladať, že tento strom je binárny, teda každý
        vrchol má najviac dvoch synov.

        Môže as stať, že strom $T$ pozostáva jedine z koreňa --
        odmieta prázdnu klauzulu a v tomto prípade veta platí.
        Teraz predpokladajme, že strom $T$ je konečný a má viac ako 1 vrchol.
        V tomto prípade má aspoň jeden akceptujúci vrchol.

        Predpokladajme, že by tento strom nemal akceptujúci vrchol.
        Potom každý vrchol obsahuje nasledovníka, ktorý nie je odmietajúci.
        Tým pádom ale môžeme vytvoriť nekonečne dlhú vetvu,
        čo je spor s konečnosťou stromu $T$.

        Množine $I(v)$ pre akceptujúci vrchol $v$
        zodpovedá čiastočná interpretácia končiaca v tom vrchole.
        Nech $v_1$, $v_2$ sú odmietajúci nasledovníci vrcholu $v$
        (spomeňme si na predpoklad, že strom je binárny).
        Čiastočné interpretácie $I(v)$, $I(v_1)$, $I(v_2)$ vyzerajú
        nasledovne:
        \begin{align*}
            I(v)    &= \{ m_1, m_2, \ldots, m_n \} \\
            I(v_1)  &= \{ m_1, m_2, \ldots, m_n, m_{n+1} \}  \\
            I(v_2)  &= \{ m_1, m_2, \ldots, m_n, \neg m_{n+1} \} 
        \end{align*}

        Zoberme teraz $C_1'$ a $C_2'$
        (základné inštancie klauzúl $C_1$ a $C_2$), ktoré nie sú
        odmietnuté v $I(v)$ ale sú odmietnuté v $I(v_1)$ resp.
        $I(v_2)$. Potom $C_1'$ musí obsahovať $\neg m_{n+1}$ a
        $C_2'$ musí obsahovať $m_{n+1}$. Položíme
        $L_1' = \neg m_{n+1}$ a $L_2' = m_{n+1}$. Dostávame tak
        rezolventu 
        \begin{equation*}
            C' = (C_1' - L_1') \cup (C_2' = L_2')
        \end{equation*}
        o ktorej vieme, že musí byť nepravdivá v $I(v)$.
        Podľa predchádzajúcej lemy musí existovať rezolventa $C$ taká,
        že $C'$ je základná inštancia $C$.

        Zoberme teraz nový sémantický strom $T'$, ktorý dostaneme
        pre množinu $S \union \{ C \}$ tak, že odstrihneme strom $T$
        vo vrchole zodpovedajúcemu rezolvente $C$.
        Tento strom bude menší a teda
        opakovaním postupu sa nakoniec dostaneme až k stromu s jedným
        vrcholom. A o tom sme už prehlásili, že vtedy veta platí.
    \end{itemize}
\end{dokaz}

\begin{priklad}
    Majme nasledujúce formuly:
    \begin{align*}
        F_1: &(\forall x) (C(x) \implies (W(x) \land R(x))\\
        F_2: &(\exists x) (C(x) \land Q(x)) \\
        G:   &(\exists x) (Q(x) \land R(x))
    \end{align*}
    Ukážte, že $G$ je logickým dôsledkom $F_1$ a $F_2$.

    Riešenie: Budeme ukazovať nesplniteľnosť $F_1 \land F_2 \land \neg G$.
    Pre $F_1$, $F_2$ a $\neg G$ vytvoríme štandardné formy.
    $F_1$ si upravíme takto:
    \begin{equation*}
    \begin{split}
        (\forall x) (C(x) \implies (W(x) \land R(x))
        & \iff (\forall x)(\neg C(x) \lor (W(x)\land R(x)) \\
        & \iff (\forall x) ((\neg C(x) \lor W(x)) \land (\neg C(x) \lor R(x)))
    \end{split}
    \end{equation*}
    Štandardná forma je teda 
    $\{\neg C(x) \lor W(x),\ \neg C(x) \lor R(x)\}$.
    Štandardná forma $F_2$ je $\{C(a),\ Q(a)\}$.
    Pre $\neg G$ dostávame
    \begin{equation*}
        \neg G \iff \neg (\exists x)(Q(x)\land R(x)) \iff 
            (\forall x) (\neg Q(x) \lor \neg R(x))
    \end{equation*}
    Štandardná formula pre túto formulu je $\neg Q(x) \lor \neg R(x)$

    Dostávame nasledujúcich 5 klauzúl:
    \begin{itemize}
        \item[1] $\neg C(x) \lor W(x)$ -- $F_1$
        \item[2] $\neg C(x) \lor R(x)$ -- $F_1$
        \item[3] $C(a)$ -- $F_2$
        \item[4] $Q(a)$ -- $F_2$
        \item[5] $\neg Q(x) \lor \neg R(x)$ -- $G$
    \end{itemize}

    Teraz budeme postupne robiť rezolventy:
    \begin{itemize}
        \item[6] $R(a)$ -- rezolventa 2, 3
        \item[7] $\neg R(a)$ -- rezolventa 4, 5
        \item[8] $\eps$ -- rezolventa 6, 7
    \end{itemize}

    \noindent
    Záver: $G$ je logickýkm dôsledkom $F_1$ a $F_2$.
\end{priklad}

